(declare-const Str2 String)
(declare-const Str6 String)
(declare-const Str12 String)
(declare-const Str14 String)
(declare-const Str16 String)
(declare-const Str17 String)
(assert (>= (str.len Str6) 25))
(assert (>= (str.len Str17) 39))
(declare-const i8 Int)
(push)
(assert (>= (str.len (str.++ Str17 (str.++ Str14 "rafmob" Str14 "nkfnfc" Str12))) i8))
(assert (>= (str.len Str16) 9))
(assert (not (str.< (str.++ Str14 "rafmob" Str14 "nkfnfc" Str12) Str2)))
(check-sat)
